[Alpuente, Escobar & Lucas - WRLA'02, Example 6.15]

Example 6.15 in [Alpuente, Escobar & Lucas - WRLA'02]

Summary: Ex6_15_AEL02

CS-TRS Ex6_15_AEL02 (file Ex6_15_AEL02.csr)

Functions:  sel s cons 0 first nil from sel1 quote first1 nil1 cons1 01 quote1 
s1 unquote unquote1 fcons

Constructors:  s cons 0 nil nil1 cons1 01 s1

Variables:  X Y Z

Arities: 

ar(sel) = 2
ar(s) = 1
ar(cons) = 2
ar(0) = 0
ar(first) = 2
ar(nil) = 0
ar(from) = 1
ar(sel1) = 2
ar(quote) = 1
ar(first1) = 2
ar(nil1) = 0
ar(cons1) = 2
ar(01) = 0
ar(quote1) = 1
ar(s1) = 1
ar(unquote) = 1
ar(unquote1) = 1
ar(fcons) = 2

Replacement map: 

µ(sel)={1,2}
µ(s)={1}
µ(cons)={1}
µ(0)={}
µ(first)={1,2}
µ(nil)={}
µ(from)={1}
µ(sel1)={1,2}
µ(quote)={}
µ(first1)={1,2}
µ(nil1)={}
µ(cons1)={1,2}
µ(01)={}
µ(quote1)={}
µ(s1)={1}
µ(unquote)={1}
µ(unquote1)={1}
µ(fcons)={1,2}

Rules:  (file Ex6_15_AEL02)   

sel(s(X),cons(Y,Z)) -> sel(X,Z)
sel(0,cons(X,Z)) -> X
first(0,Z) -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
from(X) -> cons(X,from(s(X)))
sel1(s(X),cons(Y,Z)) -> sel1(X,Z)
sel1(0,cons(X,Z)) -> quote(X)
first1(0,Z) -> nil1
first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,Z))
quote(0) -> 01
quote1(cons(X,Z)) -> cons1(quote(X),quote1(Z))
quote1(nil) -> nil1
quote(s(X)) -> s1(quote(X))
quote(sel(X,Z)) -> sel1(X,Z)
quote1(first(X,Z)) -> first1(X,Z)
unquote(01) -> 0
unquote(s1(X)) -> s(unquote(X))
unquote1(nil1) -> nil
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
fcons(X,Z) -> cons(X,Z)

The CS-TRS in OBJ format (file Ex6_15_AEL02.obj):

obj Ex6_15_AEL02 is
  sorts S .
  ops 0 0' : -> S .
  ops s s' : S -> S .
  ops nil nil' : -> S .
  op cons : S S -> S [strat (1 0)] .
  op cons' : S S -> S .
  op fcons : S S -> S .
  op from : S -> S .
  ops sel sel' : S S -> S .
  ops first first' : S S -> S .
  op quote : S -> S [strat (0)] .
  op unquote : S -> S .
  op quote' : S -> S [strat (0)] .
  op unquote' : S -> S .
  vars X Y : S .
  var Z : S .
  eq sel(s(X),cons(Y,Z)) = sel(X,Z) .
  eq sel(0,cons(X,Z)) = X .
  eq first(0,Z) = nil .
  eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
  eq from(X) = cons(X,from(s(X))) .
  eq sel'(s(X),cons(Y,Z)) = sel'(X,Z) .
  eq sel'(0,cons(X,Z)) = quote(X) .
  eq first'(0,Z) = nil' .
  eq first'(s(X),cons(Y,Z)) = cons'(quote(Y),first'(X,Z)) .
  eq quote(0) = 0' .
  eq quote'(cons(X,Z)) = cons'(quote(X),quote'(Z)) .
  eq quote'(nil) = nil' .
  eq quote(s(X)) = s'(quote(X)) .
  eq quote(sel(X,Z)) = sel'(X,Z) .
  eq quote'(first(X,Z)) = first'(X,Z) .
  eq unquote(0') = 0 .
  eq unquote(s'(X)) = s(unquote(X)) .
  eq unquote'(nil') = nil .
  eq unquote'(cons'(X,Z)) = fcons(unquote(X),unquote'(Z)) .
  eq fcons(X,Z) = cons(X,Z) .
endo

Negative results

  1. The µ-termination of Ex6_15_AEL02 cannot be proved by using Lucas' transformation. The TRS Ex6_15_AEL02_L: 
        sel(s(X),cons(Y)) -> sel(X,Z)
    sel(0,cons(X)) -> X
    first(0,Z) -> nil
    first(s(X),cons(Y)) -> cons(Y)
    from(X) -> cons(X)
    sel1(s(X),cons(Y)) -> sel1(X,Z)
    sel1(0,cons(X)) -> quote
    first1(0,Z) -> nil1
    first1(s(X),cons(Y)) -> cons1(quote,first1(X,Z))
    quote -> 01
    quote1 -> cons1(quote,quote1)
    quote1 -> nil1
    quote -> s1(quote)
    quote -> sel1(X,Z)
    quote1 -> first1(X,Z)
    unquote(01) -> 0
    unquote(s1(X)) -> s(unquote(X))
    unquote1(nil1) -> nil
    unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
    fcons(X,Z) -> cons(X)
    contains extra variables.

Positive results

  1. The µ-termination of Ex6_15_AEL02 is proved in [Bor03,Example 3.3.26] by using CSRPO:
    • marking map: 
      	   m(cons,2)=m(_cons,2)=m(quote1,1)=m(_quote1,1)={from}
    • precedence: 
      	   sel = sel1 > from, quote
	   first = first1 > cons, from, nil, cons1, nil1, quote
	   from > _from, cons, s
	   quote > 01, s1
	   quote1 > cons1, nil1
	   fcons > cons
	   unquote = unquote1 > 0, s, nil, fcons
    • status: 
      	   st(f) = lex for all symbol f.